\begin{tabbing}
$\forall$\=${\it es}$:ES, $T$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindtype($i$;$k$)$\rightarrow$state@$i$$\rightarrow$state@$i$),\+
\\[0ex]$S$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindtype($i$;$k$)$\rightarrow$state@$i$$\rightarrow$(Msg List)),
\\[0ex]$C$:($i$,$b$:Id$\rightarrow$state@$i$$\rightarrow$(kindtype($i$;locl($b$))+Unit)).
\-\\[0ex]($\forall$$e$:E. state after $e$ $=$ $T$(loc($e$),kind($e$),val($e$),(state when $e$)))
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]islocal(kind($e$))
\\[0ex]$\Rightarrow$ \=isl($C$(loc($e$),act(kind($e$)),(state when $e$)))\+
\\[0ex]\& val($e$) $=$ outl($C$(loc($e$),act(kind($e$)),(state when $e$))) $\in$ valtype($e$))
\-\-\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]isrcv(kind($e$))
\\[0ex]$\Rightarrow$ ($\langle$lnk(kind($e$))$,\,$tag(kind($e$))$,\,$val($e$)$\rangle$ $\in$ \=$S$\+
\\[0ex](loc(sender($e$))
\\[0ex],kind(sender($e$))
\\[0ex],val(sender($e$))
\\[0ex],(state when sender($e$)))))
\-\-\\[0ex]$\Rightarrow$ (\=$\forall$$a$:Atom1, $e$:E.\+
\\[0ex](\=(state when $e$):state@loc($e$)$>>$$a$\+
\\[0ex]$\Rightarrow$ $\neg$first($e$)
\\[0ex]$\Rightarrow$ \=$T$(loc($e$)):$k$:Knd$\rightarrow$kindtype(loc($e$);$k$)$\rightarrow$state@loc($e$)$\rightarrow$state@loc($e$)$>>$$a$\+
\\[0ex]$\vee$ $C$(loc($e$)):$b$:Id$\rightarrow$state@loc($e$)$\rightarrow$(kindtype(loc($e$);locl($b$))+Unit)$>>$$a$
\\[0ex]$\vee$ (state when pred($e$)):state@loc(pred($e$))$>>$$a$
\\[0ex]$\vee$ isrcv(pred($e$)) \& val(pred($e$)):valtype(pred($e$))$>>$$a$)
\-\-\\[0ex]\& (\=$e$ sends $a$\+
\\[0ex]$\Rightarrow$ \=$S$(loc($e$)):$k$:Knd$\rightarrow$kindtype(loc($e$);$k$)$\rightarrow$state@loc($e$)$\rightarrow$(Msg List)$>>$$a$\+
\\[0ex]$\vee$ $C$(loc($e$)):$b$:Id$\rightarrow$state@loc($e$)$\rightarrow$(kindtype(loc($e$);locl($b$))+Unit)$>>$$a$
\\[0ex]$\vee$ (state when $e$):state@loc($e$)$>>$$a$
\\[0ex]$\vee$ isrcv($e$) \& val($e$):valtype($e$)$>>$$a$))
\-\-\-
\end{tabbing}